InforLorV4, Main, Exploration, bibRecord, 005607

Efficient theory combination via boolean search

Identifieur interne : 005607 ( Main/Exploration ); précédent : 005606; suivant : 005608

Efficient theory combination via boolean search

Auteurs : Marco Bozzano [Italie] ; Roberto Bruttomesso [Italie] ; Alessandro Cimatti [Italie] ; Tommi Junttila [Finlande] ; Silvio Ranise [France] ; Peter Van Rossum [Pays-Bas] ; Roberto Sebastiani [Italie]

Source :

Information and computation : (Print) [ 0890-5401 ] ; 2006.

RBID : Pascal:06-0527636

Descripteurs français

Pascal (Inist)
- Quantificateur, Intégration, Assignation, Décision, Modification, Etat actuel, Raisonnement, Arithmétique, Nombre entier, Méthode optimisation, Optimisation, Variété, Implémentation, Performance, Informatique théorique, Combinaison booléenne, Satisfiabilité, 03C10, 03C80, 28XX, Vérité, Procédure décision, Variable partagée, 68T37, 49XX, 65Kxx, Splitting.
Wicri :
- topic : Décision.

English descriptors

KwdEn :
- Arithmetics, Assignment, Computer theory, Decision, Implementation, Integer, Integration, Modification, Optimization, Optimization method, Performance, Quantifier, Reasoning, Splitting, State of the art, Variety.

Abstract

Many approaches to deciding the satisfiability of quantifier-free formulae with respect to a background theory T-also known as Satisfiability Modulo Theory, or SMT(T)-rely on the integration between an enumerator of truth assignments and a decision procedure for conjunction of literals in T. When the background theory T is the combination T₁ U T₂ of two simpler theories, the approach is typically instantiated by means of a theory combination schema (e.g. Nelson-Oppen, Shostak). In this paper we propose a new approach to SMT(T₁ U T₂), where the enumerator of truth assignments is integrated with two decision procedures, one for T₁ and one for T₂, acting independently from each other. The key idea is to search for a truth assignment not only to the atoms occurring in the formula, but also to all the equalities between variables which are shared between the theories. This approach is simple and expressive: for instance, no modification is required to handle non-convex theories (as opposed to traditional Nelson-Oppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on state-of-the-art boolean and SMT search techniques, and on theory layering (i.e., cheaper reasoning first, and more often). We provide thorough experimental evidence to support our claims: we instantiate the framework with two decision procedures for the combinations of Equality and Uninterpreted Functions (εUF) and Linear Arithmetic (L A), both for (the convex case of) reals and for (the non-convex case of) integers; we analyze the impact of the different optimizations on a variety of test cases; and we compare the approach with state-of-the-art competitor tools, showing that our implemented tool compares positively with them, sometimes with dramatic gains in performance.

Affiliations:

Links toward previous steps (curation, corpus...)

to stream PascalFrancis, to step Corpus: 000414
to stream PascalFrancis, to step Curation: 000619
to stream PascalFrancis, to step Checkpoint: 000388
to stream Main, to step Merge: 005793
to stream Main, to step Curation: 005607

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Efficient theory combination via boolean search</title>
<author><name sortKey="Bozzano, Marco" sort="Bozzano, Marco" uniqKey="Bozzano M" first="Marco" last="Bozzano">Marco Bozzano</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>ITC-IRST, Via Sommarive 18</s1>
<s2>38050 Trento</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>38050 Trento</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Bruttomesso, Roberto" sort="Bruttomesso, Roberto" uniqKey="Bruttomesso R" first="Roberto" last="Bruttomesso">Roberto Bruttomesso</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>ITC-IRST, Via Sommarive 18</s1>
<s2>38050 Trento</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>38050 Trento</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Cimatti, Alessandro" sort="Cimatti, Alessandro" uniqKey="Cimatti A" first="Alessandro" last="Cimatti">Alessandro Cimatti</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>ITC-IRST, Via Sommarive 18</s1>
<s2>38050 Trento</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>38050 Trento</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Junttila, Tommi" sort="Junttila, Tommi" uniqKey="Junttila T" first="Tommi" last="Junttila">Tommi Junttila</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Helsinki University of Technology, P.O.Box 5400</s1>
<s2>02015</s2>
<s3>FIN</s3>
<sZ>4 aut.</sZ>
</inist:fA14>
<country>Finlande</country>
<wicri:noRegion>02015</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
<affiliation wicri:level="3"><inist:fA14 i1="03"><s1>LORIA and INRIA-Lorraine, 615, rue du Jardin Botanique, BP 101</s1>
<s2>54602 Villers les Nancy</s2>
<s3>FRA</s3>
<sZ>5 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Villers les Nancy</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Van Rossum, Peter" sort="Van Rossum, Peter" uniqKey="Van Rossum P" first="Peter" last="Van Rossum">Peter Van Rossum</name>
<affiliation wicri:level="1"><inist:fA14 i1="04"><s1>Radboud University Nijmegen, Toernoolveld 1</s1>
<s2>6525 ED Nijmegen</s2>
<s3>NLD</s3>
<sZ>6 aut.</sZ>
</inist:fA14>
<country>Pays-Bas</country>
<wicri:noRegion>6525 ED Nijmegen</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Sebastiani, Roberto" sort="Sebastiani, Roberto" uniqKey="Sebastiani R" first="Roberto" last="Sebastiani">Roberto Sebastiani</name>
<affiliation wicri:level="1"><inist:fA14 i1="05"><s1>DIT Universita di Trento, Via Sommarive 14</s1>
<s2>38050 Trento</s2>
<s3>ITA</s3>
<sZ>7 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>38050 Trento</wicri:noRegion>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">06-0527636</idno>
<date when="2006">2006</date>
<idno type="stanalyst">PASCAL 06-0527636 INIST</idno>
<idno type="RBID">Pascal:06-0527636</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000414</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000619</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000388</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000388</idno>
<idno type="wicri:doubleKey">0890-5401:2006:Bozzano M:efficient:theory:combination</idno>
<idno type="wicri:Area/Main/Merge">005793</idno>
<idno type="wicri:Area/Main/Curation">005607</idno>
<idno type="wicri:Area/Main/Exploration">005607</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Efficient theory combination via boolean search</title>
<author><name sortKey="Bozzano, Marco" sort="Bozzano, Marco" uniqKey="Bozzano M" first="Marco" last="Bozzano">Marco Bozzano</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>ITC-IRST, Via Sommarive 18</s1>
<s2>38050 Trento</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>38050 Trento</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Bruttomesso, Roberto" sort="Bruttomesso, Roberto" uniqKey="Bruttomesso R" first="Roberto" last="Bruttomesso">Roberto Bruttomesso</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>ITC-IRST, Via Sommarive 18</s1>
<s2>38050 Trento</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>38050 Trento</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Cimatti, Alessandro" sort="Cimatti, Alessandro" uniqKey="Cimatti A" first="Alessandro" last="Cimatti">Alessandro Cimatti</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>ITC-IRST, Via Sommarive 18</s1>
<s2>38050 Trento</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>38050 Trento</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Junttila, Tommi" sort="Junttila, Tommi" uniqKey="Junttila T" first="Tommi" last="Junttila">Tommi Junttila</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Helsinki University of Technology, P.O.Box 5400</s1>
<s2>02015</s2>
<s3>FIN</s3>
<sZ>4 aut.</sZ>
</inist:fA14>
<country>Finlande</country>
<wicri:noRegion>02015</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
<affiliation wicri:level="3"><inist:fA14 i1="03"><s1>LORIA and INRIA-Lorraine, 615, rue du Jardin Botanique, BP 101</s1>
<s2>54602 Villers les Nancy</s2>
<s3>FRA</s3>
<sZ>5 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Villers les Nancy</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Van Rossum, Peter" sort="Van Rossum, Peter" uniqKey="Van Rossum P" first="Peter" last="Van Rossum">Peter Van Rossum</name>
<affiliation wicri:level="1"><inist:fA14 i1="04"><s1>Radboud University Nijmegen, Toernoolveld 1</s1>
<s2>6525 ED Nijmegen</s2>
<s3>NLD</s3>
<sZ>6 aut.</sZ>
</inist:fA14>
<country>Pays-Bas</country>
<wicri:noRegion>6525 ED Nijmegen</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Sebastiani, Roberto" sort="Sebastiani, Roberto" uniqKey="Sebastiani R" first="Roberto" last="Sebastiani">Roberto Sebastiani</name>
<affiliation wicri:level="1"><inist:fA14 i1="05"><s1>DIT Universita di Trento, Via Sommarive 14</s1>
<s2>38050 Trento</s2>
<s3>ITA</s3>
<sZ>7 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<wicri:noRegion>38050 Trento</wicri:noRegion>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Information and computation : (Print)</title>
<title level="j" type="abbreviated">Inf. comput. : (Print)</title>
<idno type="ISSN">0890-5401</idno>
<imprint><date when="2006">2006</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Information and computation : (Print)</title>
<title level="j" type="abbreviated">Inf. comput. : (Print)</title>
<idno type="ISSN">0890-5401</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Arithmetics</term>
<term>Assignment</term>
<term>Computer theory</term>
<term>Decision</term>
<term>Implementation</term>
<term>Integer</term>
<term>Integration</term>
<term>Modification</term>
<term>Optimization</term>
<term>Optimization method</term>
<term>Performance</term>
<term>Quantifier</term>
<term>Reasoning</term>
<term>Splitting</term>
<term>State of the art</term>
<term>Variety</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Quantificateur</term>
<term>Intégration</term>
<term>Assignation</term>
<term>Décision</term>
<term>Modification</term>
<term>Etat actuel</term>
<term>Raisonnement</term>
<term>Arithmétique</term>
<term>Nombre entier</term>
<term>Méthode optimisation</term>
<term>Optimisation</term>
<term>Variété</term>
<term>Implémentation</term>
<term>Performance</term>
<term>Informatique théorique</term>
<term>Combinaison booléenne</term>
<term>Satisfiabilité</term>
<term>03C10</term>
<term>03C80</term>
<term>28XX</term>
<term>Vérité</term>
<term>Procédure décision</term>
<term>Variable partagée</term>
<term>68T37</term>
<term>49XX</term>
<term>65Kxx</term>
<term>Splitting</term>
</keywords>
<keywords scheme="Wicri" type="topic" xml:lang="fr"><term>Décision</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Many approaches to deciding the satisfiability of quantifier-free formulae with respect to a background theory T-also known as Satisfiability Modulo Theory, or SMT(T)-rely on the integration between an enumerator of truth assignments and a decision procedure for conjunction of literals in T. When the background theory T is the combination T<sub>1</sub>
 U T<sub>2</sub>
 of two simpler theories, the approach is typically instantiated by means of a theory combination schema (e.g. Nelson-Oppen, Shostak). In this paper we propose a new approach to SMT(T<sub>1</sub>
 U T<sub>2</sub>
), where the enumerator of truth assignments is integrated with two decision procedures, one for T<sub>1</sub>
 and one for T<sub>2</sub>
, acting independently from each other. The key idea is to search for a truth assignment not only to the atoms occurring in the formula, but also to all the equalities between variables which are shared between the theories. This approach is simple and expressive: for instance, no modification is required to handle non-convex theories (as opposed to traditional Nelson-Oppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on state-of-the-art boolean and SMT search techniques, and on theory layering (i.e., cheaper reasoning first, and more often). We provide thorough experimental evidence to support our claims: we instantiate the framework with two decision procedures for the combinations of Equality and Uninterpreted Functions (εUF) and Linear Arithmetic (L A), both for (the convex case of) reals and for (the non-convex case of) integers; we analyze the impact of the different optimizations on a variety of test cases; and we compare the approach with state-of-the-art competitor tools, showing that our implemented tool compares positively with them, sometimes with dramatic gains in performance.</div>
</front>
</TEI>
<affiliations><list><country><li>Finlande</li>
<li>France</li>
<li>Italie</li>
<li>Pays-Bas</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Villers les Nancy</li>
</settlement>
</list>
<tree><country name="Italie"><noRegion><name sortKey="Bozzano, Marco" sort="Bozzano, Marco" uniqKey="Bozzano M" first="Marco" last="Bozzano">Marco Bozzano</name>
</noRegion>
<name sortKey="Bruttomesso, Roberto" sort="Bruttomesso, Roberto" uniqKey="Bruttomesso R" first="Roberto" last="Bruttomesso">Roberto Bruttomesso</name>
<name sortKey="Cimatti, Alessandro" sort="Cimatti, Alessandro" uniqKey="Cimatti A" first="Alessandro" last="Cimatti">Alessandro Cimatti</name>
<name sortKey="Sebastiani, Roberto" sort="Sebastiani, Roberto" uniqKey="Sebastiani R" first="Roberto" last="Sebastiani">Roberto Sebastiani</name>
</country>
<country name="Finlande"><noRegion><name sortKey="Junttila, Tommi" sort="Junttila, Tommi" uniqKey="Junttila T" first="Tommi" last="Junttila">Tommi Junttila</name>
</noRegion>
</country>
<country name="France"><region name="Grand Est"><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
</region>
</country>
<country name="Pays-Bas"><noRegion><name sortKey="Van Rossum, Peter" sort="Van Rossum, Peter" uniqKey="Van Rossum P" first="Peter" last="Van Rossum">Peter Van Rossum</name>
</noRegion>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005607 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005607 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Pascal:06-0527636
   |texte=   Efficient theory combination via boolean search
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Efficient theory combination via boolean search

Efficient theory combination via boolean search

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri